Nuprl Definition : alle-between2 11,40
e[e1,e2].P(e) == e:es-E(es). es-le(es; e1; e)  es-le(es; e; e2)  P(e) 
latex

clarification:

alle-between2(es;e1;e2;e.P(e)) == e:es-E(es). es-le(es; e1; e)  es-le(es; e; e2)  P(e) 
latex

Definitionsx:A. B(x), es-E(es), P  Q, es-le(es; e; e')
FDL editor aliasesalle-between2

origin